(define-fun a () Int 10) 
(define-fun b () Int 0) 
(define-fun c () Int 1) 
(define-fun d () Int 5) 
(declare-fun s0 () Int)       
(define-fun e () Int 0) 
(define-fun f () Int (- s0 )) 
(define-fun u () Int f ) 
(define-fun g () Int u ) 
(define-fun h () Bool (<= g d)) 
(define-fun i () Int f ) 
(define-fun j () Int i) 
(define-fun k () Int (+ c j)) 
(define-fun l () Int (ite h k j)) 
(define-fun m () Int l) 
(define-fun n () Int (div m a)) 
(define-fun o () Bool (>= m b)) 
(define-fun p () Bool o ) 
(define-fun q () Int (ite p b c)) 
(define-fun r () Int (* n q)) 
(define-fun s () Bool (distinct e r)) 
(define-fun t () Bool s ) 
(assert t)
(check-sat)